En esta sección presentamos un ejemplo de ejecución de la herramienta, con el objetivo de ayudar a entender el 
funcionamiento de los componentes del sistema antes explicados. Dada la estructura en pipeline de la herramienta,
 mostraremos y comentaremos los resultados de cada fase de la ejecución. 

El ejemplo propuesto consiste en un juego de mesa, compuesto por un tablero, unos jugadores y sobre el tablero se 
tienen fichas de los jugadores. El tablero de juego tiene forma rectangular, y está compuesto por casillas, indexadas por 
su número de columna y número de fila (coordenadas \cod{x} e \cod{y} respectivamente). En cada casilla del tablero sólo puede haber una 
ficha de un jugador, pero un jugador puede tener varias fichas sobre el tablero. Supongamos que el juego se gestiona 
mediante una base de datos, en la que se tienen las siguientes tablas para almacenar los jugadores y el estado del 
tablero:

{\small
\begin{verbatim}
create table player {  id int primary key  };

create table board {
  int x,
  int y,
  int id,
  primary key x,y;
  foreign key(id) references player(id);
  };
\end{verbatim}
}

dónde \cod{x,y} son las coordenadas de la pieza del jugador identificado mediante \cod{id} en el tablero.

Una de las situaciones del juego consiste en eliminar a los jugadores tengan todas sus fichas amenazadas. Una ficha está amenazada si tiene la misma coordenada \cod{x} o la misma coordenada \cod{y} que alguna 
ficha de otro jugador. Las dos vistas siguientes seleccionan los jugadores que cumplen con estas premisas:

{\small
\begin{verbatim}
create view nowPlaying(id) as
  select p.id
  from player p
  where exists (select b.id from board b where b.id=p.id);

create view checked(id) as
  select p.id
  from player p
  where exists (select n.id from nowPlaying n where n.id = p.id) and
        not exists (select b1.id from board b1
                    where b1.id = p.id and
                          not exists
                         (select b2.id from board b2
                          where (b2.x - b1.x) * (b2.y-b1.y)=0 and
                                (b1.id <> b2.id)));
\end{verbatim}
}

%\end{example}

Supongamos que el usuario ejecuta nuestra herramienta con un fichero de entrada \cod{input.sql} con las anteriores sentencias SQL (
detallado en el apéndice \ref{app:sec:input}). Este fichero será analizado por el analizador SQL, generando como 
resultado una estructura C++ que representa las definiciones de tablas y vistas SQL que contiene. Por simplicidad, 
supongamos que el usuario indica a la herramienta que la tabla \cod{player} y la tabla \cod{board} tienen dos filas 
como máximo, y que el rango de los atributos de ambas tablas es de $[1,5]$. La representación C++ inherente a 
las sentencias SQL que contiene el fichero \cod{input.sql} puede consultarse en el apéndice \ref{app:sec:estructuracpp}.

Una vez que el analizador SQL ha generado la anterior representación C++, el módulo generador de fórmulas tomará 
como entrada esta estructura y el nombre de la tabla o vista SQL de la cual se quiere generar un caso de prueba. 
En nuestro caso, generaremos un caso de prueba para la vista \cod{checked}, por ser la de mayor interés.

La generación de fórmulas de restricciones para una vista, viene determinada por la tablas y vistas de las que depende, 
es decir, las que forman la cláusula \cod{from}, además de la expresión de la cláusula \cod{where}. Estas dependencias 
se pueden representar mediante un grafo, tal y como se puede ver en la figura \ref{fig:dependencias}. 

\begin{figure}
  \centering
    \includegraphics[width=0.5\textwidth]{dependencias}
    \caption{Grafo de dependencias entre las tablas \cod{player} y \cod{board} y las vistas \cod{nowPlaying} y \cod{
checked} del ejemplo propuesto.}
    \label{fig:dependencias}
\end{figure}

A continuación ilustraremos cómo generaría nuestra herramienta la fórmula de la vista \cod{checked}. Por simplicidad, 
explicaremos cómo se genera la fórmula correspondiente para cada uno de sus componentes, de forma que en el último paso 
se compondrían en una única fórmula. Señalar también que las fórmulas 
expuestas no están completas, pues se corresponden a fragmentos interesantes de las misma. Estos fragmentos pertenecen 
a la primera fila de cada fórmula, por ser el resto de filas duales. Se puede consultar la fórmula entera en el 
apéndice \ref{app:sec:formulas}. La notación para representar las filas ha sido adoptada de \cite{flops2010}, en la 
cual una fila es una substitución de la forma:

\begin{center}
\cod{\{x $\rightarrow$ expr\}} 
\end{center}

Esta notación indica que la variable simbólica \cod{x} se sustituye por la expresión \cod{expr}.

La primera fórmula que procedemos a explicar se corresponde con la tabla \cod{player} (ver \ref{app:sec:formulaplayer}).
 La primera fila de la tabla:

\begin{center}
\cod{\{player.id $\rightarrow$ player.id.0\}}
\end{center}

representa la sustitución de la variable simbólica \cod{player.id} por el valor que tiene el campo \cod{id} de la 
fila número 0 en la tabla \cod{player}. En la fórmula se indica que dos jugadores no pueden tener un mismo \cod{id}, es 
decir, no puede haber dos filas de la tabla con el mismo valor en el campo \cod{id}. Para la primera fila de la tabla, 
se tiene:

\begin{center}
\cod{player.id.0 != player.id.1} 
\end{center}

Esto es así por que, en la definición SQL, se indica que el atributo \cod{id} de la tabla \cod{player} es clave 
primaria:

{\small \noindent
\begin{verbatim}
  #(player)={(player.id.0 != player.id.1), {player.id -> player.id.0}), ...}
\end{verbatim}
}

Veamos ahora como sería la fórmula para la tabla \cod{board} (ver \ref{app:sec:formulaboard}). La primera fila de la 
tabla:

\begin{center}
\cod{\{board.x $\rightarrow$ board.x.0, board.y $\rightarrow$ board.y.0, board.id $\rightarrow$ board.id.0\}}
\end{center}

indica que las variables simbólicas \cod{board.x}, \cod{board.y} y \cod{board.id} se sustituyen por los valores de los 
campos \cod{x}, \cod{y} e \cod{id} de la fila número 0 de la tabla. Atendiendo a la definición de la tabla \cod{board}, 
encontramos dos tipos de restricciones. La primera restricción es de clave primaria para los atributos \cod{x e y}
, que indica que no puede haber dos piezas en la misma casilla del tablero, es decir, que tengan la misma coordenada \cod{(x,y)}. Para la primera fila:

\begin{center}
\cod{((board.x.0 != board.x.1) $\lor$ (board.y.0 != board.y.1))}
\end{center}

Por otro lado, tenemos una restricción de clave foránea para el atributo \cod{id}. Este atributo hace referencia al 
atributo \cod{id} de la tabla \cod{player}, por lo tanto, tiene que ser igual a alguno de los valores de \cod{id} de la 
filas de la tabla \cod{player}. De esta forma, para la primera fila de la tabla se tiene:

\begin{center}
\cod{((board.id.0 == player.id.0) $\lor$ (board.id.0 == player.id.1)) $\land$ 
((board.id.1 == player.id.0) $\lor$ (board.id.1 == player.id.1))}
\end{center}

Así, la fórmula tendría la siguiente forma:

{\small \noindent
\begin{verbatim}
  #(board)={
  (((((board.id.0 == player.id.0) OR (board.id.0 == player.id.1)) AND 
  ((board.id.1 == player.id.0) OR (board.id.1 == player.id.1))) AND 
  ((board.x.0 != board.x.1) OR (board.y.0 != board.y.1))),
  {board.x -> board.x.0,board.y -> board.y.0,board.id -> board.id.0}), ...}
\end{verbatim}
}

La siguiente fórmula de restricciones que mostramos corresponde a la vista auxiliar \cod{nowPlaying}. La primera fila 
que generaría esta vista (ver \ref{app:sec:formulanowplaying} para la fórmula completa):

\begin{center}
\cod{\{nowPlaying.id $\rightarrow$ player.id.0 \}}
\end{center}

nos indica que el atributo \cod{id} será sustituido por el valor del campo \cod{id} de la fila número 0 de la tabla 
\cod{player}. Esta vista indica los \cod{id}s de los jugadores que  están jugando actualmente. Como se puede observar en 
su definición o el grafo de dependencias (figura \ref{fig:dependencias}), esta vista depende de la tabla \cod{player}, y 
contiene una subconsulta existencial (clausula \cod{where}), que depende tanto de la tabla \cod{player} externa como de 
la tabla \cod{board}. La idea subyacente de esta vista es seleccionar los \cod{id} de jugadores que existan en 
el conjunto de jugadores con fichas en el tablero, es decir, para la primera fila se tiene:

\begin{center}
 \cod{(board.id.0 == player.id.0) $\lor$ (board.id.1 == player.id.0)}.
\end{center}

Así, lo fórmula para la vista \cod{nowPlaying}, tendría la forma:

{\small \noindent
\begin{verbatim}
  #(nowPlaying)={
  (((...) AND (( ... AND (board.id.0 == player.id.0)) OR (...  AND 
  (board.id.1 == player.id.0)))),{nowPlaying.id -> player.id.0}), ...}
\end{verbatim}
}

La fórmula que presentamos en último lugar se corresponde con la vista \cod{checked} (ver apéndice \ref{app:sec:formulachecked}), para la cual buscaremos un caso de prueba positivo. Cómo se puede apreciar en su definición, 
es una vista bastante compleja, con varias subconsultas anidadas, y que depende, no solo de las tablas \cod{player} y \cod{board}, si no también de la vista auxiliar \cod{nowPlaying}.  La primera fila que generaría la ejecución de esta 
vista sería:

\begin{center}
\cod{\{checked.id $\rightarrow$ player.id.0\}}
\end{center}

que asignaría a la variable simbólica \cod{checked.id} el valor del campo \cod{id} de la primera fila de la tabla \cod{
player}. El objetivo de esta vista es decidir si dos fichas, de jugadores distintos, tienen la misma coordenada \cod{x} 
o coordenada \cod{y} del tablero de juego. Esta propiedad se describe mediante la siguiente expresión: 

\begin{center}
\cod{((board.x.0 - board.x.1)*(board.y.0 - board.y.1) == 0) $\land$ (board.id.1 != board.id.0))}.
\end{center}

Así, la fórmula tendría la siguiente forma:

{\small \noindent
\begin{verbatim}
  #(checked)= {
  ( ... AND ... 
  (not (((((board.x.0 - board.x.1) * (board.y.0 - board.y.1)) == 0)
  AND (board.id.1 != board.id.0)) OR ...)),
  {checked.id -> player.id.0}), ...}
\end{verbatim}
}

En realidad, nuestra herramienta genera una única fórmula de restricciones para la tabla o vista que se seleccione. 
Como se mencionó anteriormente, si una vista depende de otras tablas o vistas, se calcularán las fórmulas de 
restricciones asociadas a estas, ya que formarán parte de la fórmula de restricciones asociada a la vista original, 
junto con la expresión que contenga la expresión de la cláusula \cod{where}. En este caso, la fórmula para la vista \cod{checked}, en una representación abstracta, podría ser:

$$\theta(checked) = \theta(nowPlaying) \land \theta(player) \land \theta(board) \land where_{checked}$$ \label{formula:
abstracta}

Continuando con nuestro ejemplo, procedemos a buscar un caso de prueba positivo para la vista \cod{checked}. Por lo tanto, tras generar su correspondiente fórmula de restricciones, se inicia la etapa de traducción 
de dicha formula al lenguaje de restricciones del resolutor específico. Para ello, elegimos MiniZinc como lenguaje de 
modelado de restricciones, pues es un lenguaje aceptado por un gran número de resolutores de restricciones. La última 
distribución incluye el resolutor G12, por lo que usaremos dicho resolutor por comodidad. De esta forma, se obtendría 
un fichero de salida, supongamos \emph{output.mzn} (ver \ref{app:sec:output}). Este fichero contiene el modelo de 
restricciones para la vista \cod{checked} en lenguaje MiniZinc, y podrá ejecutarse posteriormente, obteniendo, si 
existe, el caso de prueba positivo para dicha vista. En nuestro caso, y con el objetivo de obtener resultados 
significativos, hemos reducido el dominio de las variables simbólicas que componen el modelo MiniZinc, pudiendo éstas 
tomar valores entre 1 y 5. Tras ejecutar este fichero se obtiene el siguiente resultado:

\begin{verbatim}
INSERT INTO board(id,x,y) VALUES (1,1,1);
INSERT INTO board(id,x,y) VALUES (2,1,5);
INSERT INTO player(id) VALUES(1);
INSERT INTO player(id) VALUES(2);
\end{verbatim}\label{resultado}

Como se puede ver, el resultado está compuesto por sentencias SQL. Estas sentencias, ejecutadas en un entorno SQL, 
poblarán las tablas involucradas en la vista sobre la que se quiere obtener un caso de prueba. Cabe señalar que este 
resultado puede variar, dependiendo del resolutor usado o del método de búsqueda de la solución empleado, pero si 
existe un caso de prueba positivo, el modelo de restricciones que usamos asegura que se encuentra. Distintos casos de prueba pueden obtenerse pidiendo al resolutor que porporcione más soluciones.

Tras ejecutar las sentencias obtenidas del resolutor como resultado, la instancia de base datos que define el 
caso de prueba tendría la siguiente forma:

\begin{center}
\begin{tabular}{ll}
\begin{tabular}{|c|}
\hline
{\textbf{player}} \\
\hline
id \\
\hline
$1$ \\
$2$ \\
\hline
\end{tabular}
&
\begin{tabular}{|c|c|c|}
\hline
\multicolumn{3}{|c|}{\textbf{board}} \\
\hline
id & x & y \\
\hline
$1$ & $1$ &  $1$ \\
$2$ & $1$ &  $5$ \\
\hline
\end{tabular}
\end{tabular}
\end{center}

Con esta instancia de bases de datos, la configuración del tablero de juego tendría la configuración siguiente:

\begin{center}
\begin{tabular}{|c|c|c|c|c|}
\hline
2 &  &  &  &  \\
\hline
  &  &  &  &  \\
\hline
  &  &  &  &  \\
\hline
  &  &  &  &  \\
\hline
1 &  &  &  &  \\
\hline
\end{tabular}
\end{center}

Dónde las casillas en blanco indican que no hay fichas en ellas. Además, el jugador con \cod{id = 2} tiene un ficha en 
la casilla situada en la fila 5 y columna 1 del tablero (coordenadas \cod{(y,x)} respectivamente), mientras que el jugador 
con \cod{id = 1} tiene una ficha situada en la casilla de la fila 1 y columna 1 (coordenadas \cod{y,x} respectivamente).

Si ahora realizamos la siguiente consulta a nuestro gestor de bases de datos:

\begin{center}
\begin{verbatim}
select * from checked;
\end{verbatim}
\end{center}

El resultado que se obtendría sería:

\begin{center}
\begin{tabular}{|c|}
\hline
id \\
\hline
$1$ \\
$2$ \\
\hline
\end{tabular}
\end{center}

A la vista de la configuración del tablero, es el resultado esperado, pues el jugador con \cod{id = 1} y el jugador con 
\cod{id = 2} poseen una ficha cada uno, que además están mutuamente amenazadas.



